Reduce barriers to contributing to the standard library #86
Conversation
There was a problem hiding this comment.
A worthwhile goal. Hope you have some good discussions with the Core team and that you can identify some actionable improvements that can be done soon.
Keep in mind that almost everyone is a volunteer. Inria researchers choose what they work on; Inria managers can't tell them what to do/work on. Inria engineers can be assigned tasks, but there are only a couple that work on Coq.
|
|
||
| ### 7-day Response Window | ||
|
|
||
| In case a CI development has been unresponsive to a PR for 7 calendar days, this CI development should be routinely marked as `allow_fail`. This should not be taken as a condemnation of the downstream codebase or development team, just a necessity of developing Coq. Once the development has been updated, a PR removing the `allow_fail` tag from it should be merged as soon as CI passes on it. Note: this proviso must not be used to avoid investigating CI failures, but rather as an alternative to merging (or finalizing) a patch when the reason for the need for a change is understood thoroughly. (At the same time, the CI is not intended to be a test suite: instead of maintaining a development just to use as a test, the key parts of it that uniquely exercise Coq should be extracted and moved to the test suite). |
There was a problem hiding this comment.
"a CI development" meaning the maintainers of a particular CI package? Generally maintainers are volunteers with many other things on their plates. Some may be able to (and want to) respond quickly while others may not.
"unresponsive to a PR for 7 calendar days" - 7 days measured from when? Initial submission? Merging?
There was a problem hiding this comment.
Yes. I agree there is tension here, and maybe 7 days isn't the right number, but I do think it is important to have a practiced mechanism by which we avoid Coq/stdlib being held back by inaction elsewhere.
As for what time to count, what I have in mind is from when the external maintainers are contacted to initial technical response -- perhaps "triage" is a good way to sum it up. In the case of a simple PR (e.g. fully qualifying some paths), the response would hopefully include merging it, but not all changes are that easy, and we shouldn't rush them.
|
|
||
| # Compat Strategy | ||
|
|
||
| We should make every effort to escape the rigidity trap the stdlib is currently caught in, while maintaining the status of stdlib as a reliable piece of infrastructure to depend upon and followed through its development. Stability in the sense of avoiding change is not a goal. The median change to stdlib will require backwards-compatible changes in multiple CI developments. These changes would be routinely merged by maintainers of these developments, and co-developed by them if necessary due to complexity of their code, unusual requirements, or otherwise. Once-and-over-with strategies for CI-wide changes should be preferred of phased rollouts whenever practical, to avoid needless code churn and developer toil in both stdlib and downstream. In cases where an atomic replacement is infeasible, but there are strong reasons for making the change, a pilot rollout in representative developments should precede an add-deprecate-replace-remove cycle. No step in this process should involve waiting for another Coq release, or any specific amount of time -- if we have ported the CI and are confident that other developments can be ported, the change should proceed without delay. |
There was a problem hiding this comment.
Stability in the sense of avoiding change is not a goal.
I think the current goal is not to break existing work in a way that excessively disrupts users/maintainers. You might start by understanding/discussing the current compatibility goals. I'm not sure those goals are written out anywhere.
Coq should aim to satisfy users' needs, but users' needs vary and may conflict.
There was a problem hiding this comment.
PS Would be nice to split some of the very long lines (e.g. line 95 above).
There was a problem hiding this comment.
The best documentation I know is section 3.6 of Théo Zimmermann's dissertation. What I am proposing here is largely within the same spirit, but not identical in a number of aspects.
|
|
||
| ## External Reviewers | ||
|
|
||
| It may be the case that the Coq team is not available or equiped to review one change or another, even though the concept looks valuable. In this case anyone can suggest an external reviewer, and with the blessing of a component maintainer or core developer, this external reviewer can take care of the technical vetting aspects of the PR review process. |
There was a problem hiding this comment.
I think this is possible today--make a request and then it's at the discretion of the maintainer/internal reviewer.
|
Thank you for the kind words. I agree that volunteer time and interests are a significant constraint here, and I am aware that many other developers are not as enthusiastic about maintaining stdlib as I am. In a way, this CEP is a grab-bag of specific ideas behind the underlying question "do we even want to?" -- and if not, I too might lean towards splitting off stdlib as anticipated in #83 (but see also earlier discussion). Yet, in a number of points I asking for a blessing more than any action, and I am hopeful that there will be common ground at least that far. I have added this CEP to https://github.com/coq/coq/wiki/Coq-Call-2024-04-23. |
|
Cc @coq/stdlib-maintainers your input would be appreciated (and not all of you are watching this repository). |
Rendered